Language/OS - Multiplatform Resource Library/LANGUAGE OS.iso/quintus/quintus0.lha/work/prover_2.06.2

Text File | 1992-04-03 | 25KB | 527 lines

%%%                   Clause-Linking Prover
%%%                         (CLIN 2)
%%%
%%%            DAVID A. PLAISTED, SHIE-JUE LEE, and
%%%                   GEOFFREY D. ALEXANDER
%%%               Department of Computer Science
%%%                University of North Carolina
%%%                Chapel Hill, NC 27599--3175
%%%                 (919) 962-{1751|1934|1983}
%%%             {plaisted|lee|alexande}@cs.unc.edu
%%% (c) 1991 by Geoff Alexander, Shie-Jue Lee, and David Plaisted
%%%
%%% version 2.00.0 (based on CLIN version 19.4)
%%%   added equality transformation
%%% version 2.00.1
%%%   added equality rewriting
%%% version 2.00.2
%%%   fixed rewriting of eqaulity literals
%%% version 2.00.3
%%%   changed "equality_rewriting" to "auto_orient"
%%%   added "outrwr", "outrwt", "outtreq", and "pullout-constants"
%%% version 2.00.4
%%%   fixed priority of rewritten term
%%%   fixed input clause count when transforming equation
%%% version 2.00.5
%%%   added recurive path ordering
%%%   optimized equality transform
%%%   saved rewrite rules across sessions
%%% version 2.00.6
%%%   added user specified rewrite rules and orderings
%%%   added "include_original_clause"
%%%   changed default of "simple_small_proof_check" from clear to set
%%% version 2.00.7
%%%   moved term rewriting to hypermatching
%%% version 2.00.8
%%%   added lexicographic path ordering
%%% version 2.00.9
%%%   added bound on term rewriting
%%%   fixed bug in var_eq
%%%   moved ground from rewrite to library
%%%   moved unground from rewrite to library
%%%   simplified rewriting of equations
%%%   optimized var_eq
%%%   optimized assert_rewrite_rule
%%%   optimized generate_eq_rewrite_rules
%%% version 2.01.0
%%%   checked clause priority after each hyper-link
%%%   rewrote clauses in all round 0s instead of just session 1 round 0
%%%   fixed bug in rewrite_clauses which asserted duplicate clauses
%%% version 2.01.1
%%%   modified rewrite_lit so that only arguments of s in not s=t are rewritten
%%%   fixed transivity bug when asserting rewrite order
%%% version 2.01.2
%%%   added code to rewrite rewrite rule
%%%   fixed bug in delete_rewrite_rule which sometimes deleted the wrong rule
%%% version 2.01.3
%%%   moved generation of rewrite rules to hyper-linking
%%%   moved rewriting of input clauses to interpret
%%%   moved print_eq_trans to eq_trans
%%%   fixed bug when rewriting hyper-links from a unit nucleus
%%%   modified term_order_lpo and term_order_rpo so that order can instantiated
%%%     when calling; that is, let term_order be a test
%%%   modified code which orients equations so that an equation s=t is oriented
%%%     only when the rewrite rule t->s is generated
%%% version 2.01.4
%%%   modified rewriting of equations according to David Plaisted's method
%%%   modified assert_rewrite_rule so that it does not assert a rewrite rule
%%%     if it is an instance of an existing rewrite rule
%%%   fixed method of rewriting rewrite rules so that deleted rewrites rules
%%%     aren't generated again
%%% version 2.01.5
%%%   added code to rewrite asserted clauses
%%%   fixed bug in rewrite_asserted_clauses which caused rewritten clause to
%%%     have clause size and number of non-grounded literals swapped
%%%   fixed bug in rewrite_asserted_clauses which caused duplicate clauses to
%%%     be asserted
%%% version 2.01.6
%%%   sorted electrons by term size
%%%   fixed bug in literal_size which caused not to be counted
%%% version 2.01.7
%%%   oriented input equations literal in each direction
%%% version 2.01.8
%%%   modified rewriting of equations so that equations are fully rewritten
%%%   added transformed form of all non-input equations before hyper-linking
%%%   removed use of semi_internal_form from rewrite_asserted_clauses
%%%   recomputed variable list when rewriting hyper-link
%%%   fixed bug in duplicate_clause_C
%%% version 2.01.9
%%%   optimized term rewriting
%%% version 2.02.0
%%%   made the support and distance for pulled out equations the same as input
%%% version 2.02.1
%%%   added partial hyper-links to priority structure
%%%   asserted over_priohm if priority exceeded during rewriting or
%%%     hyper-linking
%%%   fixed bug which counted hyper-links rejected after rewriting as good
%%%   added partial rewrite count
%%%   fixed bug in rewrite_asserted_clauses which caused simplified clauses to
%%%     be printed twice
%%% version 2.02.2
%%%   asserted pulled out equations at beginning of session
%%%   deleted pulled out form when rewriting asserted clause
%%% version 2.02.3
%%%   deleted pulled out form of clauses whose priority is too large
%%% version 2.02.4
%%%   fixed bugs when updating priority structure with partial hyper-link
%%% version 2.02.5
%%%   asserted equations along with pulled out forms at beginning of session
%%%   asserted pulled out forms of equations at the beginning of each round
%%%   fixed bug when updating priority structure with partial hyper-link
%%% version 2.02.6
%%%   optimized lpo_order and rop_order by treating indentical terms as
%%%     equivalent
%%% version 2.02.7
%%%   modified code so clauses corresponding to rewrite rules are not deleted
%%%   asserted equations corresponding to rewrite rules after simplifying
%%%     rewrite rules
%%% version 2.02.8
%%%   deleted rewrite rules when the priority of the lhs exceeds the priority
%%%     bound
%%% version 2.02.9
%%%   performed time overflow check after rejecting hyper-link due to priority
%%% version 2.03.0
%%%   moved rewrite rule simplification to hyper-linking
%%%   asserted equations for rewrite rules during round 0 (except for session
%%%     1 round 0) in addtion to other rounds
%%%   performed time overflow check after rejecting hyper-link due to relevance
%%%   counted hyper-links rejected due to relevance as rejected
%%%   set user support flag correctly when asserting equations corresponding to
%%%     rewrite rules
%%%   fixed bug in lexicographical path ordering
%%% version 2.03.1
%%%   added early unit subsumption by X=X test
%%% version 2.03.2
%%%   modified rewriting of equations so that equations are fully rewritten
%%% version 2.03.3
%%%   strengthened early unit subsumption test so that partial hyper-links
%%%     having all linked negative equations linked with X=X are tested
%%%     using restricted rewrite
%%%   fixed bug in the determination of linked and unlinked literals in partial
%%%     hyper-links
%%%   removed unit nucleus optimization from proc_C as modification for
%%%     rewriting is more costly than normal processing
%%%   removed unit nucleus optimization from calculate_new_size,
%%%     calculate_priority_HM, make_varstail as it doesn't work with rewriting
%%%   removed ground hyper-link optimization from calculate_new_size and
%%%     calculate_priority_HM as it doesn't work with rewriting
%%% version 2.03.4
%%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
%%%     are visible externally -- changes to comments, predicate names, and
%%%     variable names are not incorporated
%%%   made "outrwr", "outrwt", and "outtreq" default to clear
%%%   printed deleting rewrite rule message only when outrwr set
%%%   modified deleting rewrite rule message
%%%   printed axioms
%%%   modified rewrite_clause, rewrite_clause_np, rewrite_lit, rewrite_term,
%%%     and rewrite_term_args_only so that they return immediately if there are
%%%     no rewrite rules
%%%   performed early unit subsumption test only when "equality_transform"
%%% version 2.03.5
%%%   assert equations for rewrite rules only if there are rewrite rules
%%%   removed counters
%%%   restored unit nucleus and ground nucleus optimizations to
%%%     calculate_new_size, calculate_priority_HM, make_varstail, and
%%%     proc_C when no rewrite rules
%%% version 2.03.6
%%%   increased number of variables allowed in clauses from 20 to 100
%%%   no longer include input equations in both directions
%%%   don't recalculate variable list after rewriting hyper-link as variable
%%%     list is for nucleus
%%% version 2.03.7
%%%   optimized order_term by saving order of subterms
%%% version 2.03.8
%%%   don't rewrite clauses if proof found during hyper-linking
%%%   rewrite clauses in round 0 when necessary
%%% version 2.03.9
%%%   don't update priority structure in early priority test
%%% version 2.04.0
%%%   performed unit deletion in early priority test
%%%   logically erased nuclei while hyper-linking
%%%   don't try to delete pulled out forms unless equality_transform set
%%%   changed spc time bound factor from 2 to 3
%%%   fixed bug with "outhllits"
%%%   saved input clauses between sessions same as clin 1
%%% version 2.04.1
%%%   determined maximum number of non-ground literals in a clause each round
%%%     (required for equality transform)
%%% version 2.04.2
%%%   modified rewriting of equations so that the corresponding rewrite rule
%%%     is not used
%%%   modified transform_equations_session and transform_equation_round include
%%%     pulled out forms forms for input equations
%%% version 2.04.3
%%%   when pulling out equations, ordered pulled out form so that pulled out
%%%     literals for the smaller side with respect to path order come first
%%%   added reverse/2
%%%   changed pullout_constants default value to clear
%%%   no longer need to recompute largest clause length when doing replacement
%%%   erased corresponding equation and pulled out form when simplifying
%%%     rewrite rule
%%%   fixed rmrwr_prio so it erased all rewrite rules whose lhs was larger
%%%     than the priority bound
%%%   fixed bug in logically_erase_clause_C
%%%   rewrote clause during replacement
%%%   rewrote clauses after replacement (as well as before)
%%%   removed transitivity axiom
%%%   updated priority structure when early priority test succeeds
%%% version 2.04.4
%%%   no longer pull out equations at the beginning of rounds
%%%   used restrictive method for rewriting equations
%%%   erased equation associated with rewrite rule only if equation's priority
%%%     exceeded priority bound
%%%   restored transitivity axiom
%%%   rewrote s fully before attempting to assert a rewrite rule for s=t
%%%   when replacing and rewriting, perform replacement/rewrite repeatedly
%%%     until no change
%%%   modified rewriting of s=t with s>t to handle case where rewriting s once
%%%     at outer level generates a term smaller than the normal form of t
%%% version 2.04.5
%%%   added restricted_rewrite to control whether restricted or unrestricted
%%%     rewriting of equations is used
%%%   added equality_transform_by_round flag
%%%   added safe_early_priority_test flag
%%%   added early_unit_subsumption flag
%%%   added early tautology test
%%%   fixed rewrite_asserted_clauses so it erases pulled out forms of rewritten
%%%     clauses
%%%   fixed rewrite_asserted_clauses so it pulls out rewritten input clauses
%%%   fixed rewrite_asserted_clauses so it pulls out rewritten input clauses
%%%   removed rewriting from hyper-linking
%%%   removed the generation of rewrite rules from hyper-linking
%%%   added duplicate_clauses
%%%   don't include original equations in both directions
%%%   added small_proof_nucleus_bound
%%%   corrected setting of paramters with infinity default
%%%   when pulling out equations, ordered pulled out form so that pulled out
%%%     literals for the larger side with respect to path order come first
%%% version 2.04.6
%%%   added fixed_priority
%%%   removed unnecessary checks for rewrite rules now that rewriting is no
%%%     longer done in hyper-linking
%%%   removed rewriting from replacement
%%%   added start_priority_bound
%%%   added min_list
%%%   added get_list
%%%   fixed bug in code which determines if another round of hyper-linking is
%%%     required
%%% version 2.04.7
%%%   when rewriting asserted clauses generate rewrite rules for equation in
%%%     normal form
%%%   rewrote asserted clauses after unit simplification
%%%   moved code to erase clause corresponding to rewrite rule from
%%%     erase_rewrite_rule to rmrwr_prio
%%%   modified logically_erase_clause_C_prio so that it only erases non-input
%%%     clauses
%%%   modified erase_clause_HM_prio so that it only erases non-input clauses
%%%   modified erase_clause_T_prio so that it only erases non-input clauses
%%% version 2.04.8
%%%   added group_detection
%%%   added get_subterms
%%%   improved efficiency of transform_equations_round
%%%   added duplciate_repeated_replace_rule
%%%   fixed bug in rewrite_outer which prevented priority test from being done
%%%   fixed bug in early priority test which updated priority for partial
%%%     instances which passed test instead of those which failed
%%%   rewrote partial instance before early tautology test and early priority
%%%     test
%%% version 2.04.9
%%%   don't assert a rewrite rule if its lhs or rhs has a priority greater
%%%     than the priority bound
%%%   don't assert a clause whose priority is larger than the priority bound
%%%   sorted clauses by priority before rewriting
%%% version 2.05.0
%%%   don't select a support strategy unless there is a new clause or an
%%%     existing clause has modified the appropriate support
%%%   improved the efficiency of the unit deletion in early priority test
%%%   checked for duplicate partial instances
%%%   rejected a partial instance which is an instance of a previous partial
%%%     instance only when delete_all_instances is set
%%%   ordered early tests as early priority test, early tautology test,
%%%     duplicate partial instance test, and early unit subsumption
%%%   deleted a rewrite rule if its rhs priority is larger than the priority
%%%     bound
%%%   deleted a partial instance if its priority is larger than the priority
%%%     bound
%%%   rewrote literal before linking it
%%%   erased partial instances for each nucleus
%%% version 2.05.1
%%%   added clause splitting
%%%   fixed transform_equations_round so that it works when neither
%%%     fixed_priority nor slidepriority is specified
%%%   added gensym
%%%   added common_variables
%%%   fixed assert_group_axiom so that it works when neither fixed_priority
%%%     nor slidepriority is specified
%%%   split horn clauses into horn clauses
%%% version 2.05.2
%%%   modified the top level structure of clin
%%%   added clause splitting to top_level_replacement
%%%   added clause splitting to transform_equations_round
%%%   don't rewrite clauses in group dection
%%%   fixed assert_rewrite_rule_equations so that it works when neither
%%%     fixed_priority nor slidepriority is specified
%%%   fixed bug in assert_group_properties
%%% version 2.05.3
%%%   added support for Quintus Prolog
%%%   removed print_clause_list as it is also defined in auxiliary
%%%   fixed bug which caused loop when proof found in simplification
%%%   fixed bug when updating priority structure after early priority failure
%%%   modified rmhm_prio to delete equations corresponding to rewrite rules
%%%     if their priority exceeds priority bound
%%%   modified rmhm_prio not to delete pulled out forms when deleting a clause
%%%   modified update_priority_structure to delete partial instances whose
%%%     priority exceeds the priority bound
%%%   added error check to update_priority_bound
%%%   updated priority structure with priority from partial instances not
%%%     rejected by early priority test
%%%   don't erase rewrite rules corresponding to input equations
%%%   fixed clause rewriting to run when auto_orient and no rewrite rules
%%%   don't perform early tests on unlinked partial instances
%%%   performed early unit subsumption test in get_hm_nucleus
%%%   performed partial instance check in get_hm_nucleus
%%%   no longer erased partial instances for each nucleus
%%%   replaced integer_name with name
%%%   made replacement work with fixed_priority
%%%   modified clin structure so that clause rewriting done before main
%%%     repeat loop and after simplification
%%%   fixed inst_del so it actually deletes instances
%%%   checked unit clauses in instance deletion when rewriting or replacement
%%%   assumed no instance when UR strategy, not rewriting, and no replacement
%%%   don't check for the following when delete_all_instances:
%%%    2. if C is user supported, then D is user supported
%%%    3. if C is backward supported, then D is backward supported.
%%%   fixed electron instance check so it doesn't erase and assert lit_G while
%%%     backtracking over lit_G
%%% version 2.05.4
%%%   added banner to Qunitus version
%%%   fixed bug which prevented clause_splitting option from being printed
%%%   saved split clauses as sent_c
%%%   don't erase or assert pulled out forms when rewriting clauses
%%%   don't assert duplicate input clauses including pulled out forms
%%%   rewrite rewrites rules after asserting group rewrite rule
%%%   erase rewrite rules corresponding to input equations
%%%   when rewriting clauses, erase old clause before checking priority of new
%%%     clause
%%%   when rewriting clauses, don't reject new clause if priority bound not set
%%% version 2.05.5
%%%   added equational rewriting
%%%   don't erases clause when erasing large rewrite rules
%%%   modified clin structure so generation of equations from rewrite rules
%%%     done before main repeat loop after clause rewriting
%%%   rewrite group axioms before asserting
%%%   fixed a couple of bugs which prevented equational rewriting from working
%%%   fixed bug which caused clauses to be asserted with uninstantiated size
%%%   fixed bug which prevented "satisfiable" result
%%%   don't check priority when input clause rewritten
%%%   fixed bug when rewriting input clause
%%% version 2.05.6
%%%   changed early unit subsumption to equality early unit subsumption
%%%   added new early unit subsumption
%%%   modified round 0 action
%%%   don't repeat clause generation unless more than 1 clause generation
%%%     modules requested
%%%   moved instance deletion into clause generation loop
%%%   added print after clause generation
%%% version 2.05.7
%%%   ehanced equality early unit subsumption test
%%%   don't hyper-link unit nuclei
%%%   terminated clause generation loop if proof found in replacemet
%%%   fixed minor equational rewrite bug in rewrite_lit_6
%%% version 2.05.8
%%%   improved the efficiency of order_term_lpo
%%%   removed append/3
%%%   renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
%%%   added quintus_compile_options
%%%   added write_line/5
%%%   don't assert equational rewrite rule if rhs contains variable not
%%%     contained in lhs
%%%   added priority_bound_increment
%%% version 2.05.9
%%%   fixed bug in lpo term ordering
%%%   added Quintus Prolog 3.1 support
%%%   added implementation improvement to lpo term ordering
%%%   fixed bug in rewrite_lit
%%%   fixed bug in rewrite_grounded_term_list
%%% version 2.06.0
%%%   fixed print_rewrite so that the used a consistent naming of variables for
%%%     the original and new clause
%%%   added is_subterm/2
%%%   added identical_subset/2
%%%   added identical_set_difference/3
%%%   added substitute_term/4
%%%   added identical_embedded/2
%%%   fixed bug in rewrite_outer_equational
%%%   added identical_set/2
%%%   apply once_replace_rules only once per round
%%%   added instance_clause_C/2
%%%   made delete_all/3 and identical_delete_all/3 deterministic
%%%   added cprolog support
%%%   rewrite rewrite rules only once during group detection
%%%   added garbage collect/0 for als and cprolog
%%%   fixed assert rewrite rule to print equational rules in both directions
%%%   added bug fixes from Shie-Jue
%%%   fixed bug in restricted rewriting
%%%   added write_line/6
%%%   added clause_generation_loop flag
%%%   added check_unit_conflict_C/1
%%%   added check_unit_conflict_HM/1
%%%   added early check for unit conflict
%%%   modified session 1 round 0 processing
%%%   added save_rewrite_rules
%%% version 2.06.1
%%%   added constrained rewriting
%%%   don't print fully rewritten equations and inequation under restricted
%%%     rewriting
%%%   added substitute_term_all/4
%%%   added permutations/2
%%%   added append_lists/2
%%%   added tail/2
%%%   added save_unrestricted_normal_form
%%%   added retract_all/1
%%%   added early unit conflict check to rewrite_rewrite_rules
%%%   fixed bug in check_unit_conflict_C/1 and check_unit_conflict_HM/1
%%%   fixed bug in hm_literal which sometimes erronously failed to link
%%%   rewrite group rewrite rule before asserting
%%%   fully sort nuclei before hyper-linking
%%%   rewrite replace rules
%%%   added duplicate_once_replace_rule/2
%%% version 2.06.2
%%%   fixed Quintus Prolog existence error in duplicate deletion
%%%   fixed duplicate setting of inifinity defaults
%%%   run clause generation loop in session 1 round 0
%%%   added fast_priority_update
%%%   added duplicate_partial_instance_test
%%%   added precompute_constraints
%%%   modified rewrite_lit_with_constraints so that restricted rewriting
%%%     doesn't depend on constraints
%%%   fixed Quintus Prolog existence error in instance deletion
%%%   fixed Quintus Prolog existence error in small proof checker
%%%   added restricted_equality_transform
%%%   modified priority test for non-constrained clause rewriting to check
%%%     priority of rewritten clause rather than rhs of the rewrite rule
%%%   cached lexicographical path ordering
%%%   added index and size bound to cached_rewrite
%%%   added ground_like/4
%%%   added size bound to cached_constraint_consistent
%%%   added size bound to cached_constrained_term_order and
%%%     cached_constrained_term_order_complete
%%%   don't add to constraint when constraint precomputed
%%%   cached constrained subterm rewrites
%%%   added term_size_structure/2
%%%   added enumerate/4
%%%   removed rpo code as it isn't supported (or used)
%%%   added cache_size
%%%   modified rewrite_rule_ref/2 to work with linearized rwr
%%%   fixed assert_rewrite_rules_equations/0 to assert equations for equational
%%%     rewrite rules
%%%   fixed assert_group_axiom/1 to work when priority_bound is not set
%%%   added additional time overflow tests
%%%   updated equality axioms
%%%   check for unit conflict in hyper when sliding priority not specified
%%%   changed restricted_equality_transform default to 0
%%%   added time bound for simple small proof checking
%%%   terminated small proof check if time limit exceeded
%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% ALS-Prolog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%    :- [-'/unc/alexande/research/clin/als_2.06.0'].

%%%%%%%%%%%%%%%%%%%%%%%
%%% CProlog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%
%    :- [-'/unc/alexande/research/clin/cprolog_2.06.0'].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Quintus Prolog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    :- compile('/unc/alexande/research/clin/quintus_2.05.8').
    :- compile('/unc/alexande/research/clin/quintus_compile_options_2.05.8').

%%%%%%%%%%%%%%%%%%%
%%% Common code %%%
%%%%%%%%%%%%%%%%%%%

%%% Load files.
    :- load_file('/unc/alexande/research/clin/auxiliary_2.06.2').
    :- load_file('/unc/alexande/research/clin/clausify_18.7').
    :- load_file('/unc/alexande/research/clin/command_2.06.2').
    :- load_file('/unc/alexande/research/clin/csplit_2.05.4').
    :- load_file('/unc/alexande/research/clin/exprules_18.4').
    :- load_file('/unc/alexande/research/clin/fms_2.06.0').
    :- load_file('/unc/alexande/research/clin/group_2.06.2').
    :- load_file('/unc/alexande/research/clin/hyper_2.06.2').
    :- load_file('/unc/alexande/research/clin/instdel_2.06.2').
    :- load_file('/unc/alexande/research/clin/interp_2.06.0').
    :- load_file('/unc/alexande/research/clin/library_2.06.2').
    :- load_file('/unc/alexande/research/clin/main_2.06.2').
    :- load_file('/unc/alexande/research/clin/pc_2.05.3').
    :- load_file('/unc/alexande/research/clin/replace_2.06.0').
    :- load_file('/unc/alexande/research/clin/rewrite_2.06.2').
    :- load_file('/unc/alexande/research/clin/simplify_2.06.2').
    :- load_file('/unc/alexande/research/clin/spc_2.06.2').
    :- load_file('/unc/alexande/research/clin/transform_2.06.2').
    :- load_file('/unc/alexande/research/clin/try_2.06.2').
    :- load_file('/unc/alexande/research/clin/xvisor_2.05.8').

%%% Initialization
     :- initialization(abolish(clin_version,1)).
     :- initialization(assert(clin_version('2.06.2'))).

%%% Welcome message.
     :- initialization((clin_version(Version),
    nl, tab(15),write('WELCOME TO CLIN '),
    write(Version),nl,
        write('(c) 1991 by Geoff Alexander, Shie-Jue Lee, and David Plaisted'),
    nl,nl,nl)).
     helpmsg :-
    nl,write_line(2,'USER GUIDE : '),
    write_line(2,'Key in "prove(File).".'),
    write_line(2,'Key in "settings." to list all current settings.'),
    write_line(2,'For more info., type "choice.".'),
    write_line(2,'These info. can be reviewed by typing in "helpmsg.".'),
    nl.
     :- initialization(helpmsg).